﻿module Lib.BinaryRelation where

import Lib.Logic
import Lib.Set
import Prelude hiding (id)

-- = Megjegyzések = --
--konvenció: jelölje xs a relációt
{-todo:
    - operátorok kiválogatása előre
	- elnevezések
	- ellenőrzések (kompozíció, stb)
	- munka befejezése (a függvénydefiníció-gyűjtemény nem teljes)
-}

infixr 5 !

(×) :: (Eq a1, Eq a2) => [a1] -> [a2] -> [(a1, a2)]
(×) xs ys = foldr (\a b -> (map (\y -> (a,y)) ys) ∪ b) [] xs

-- értelmezési tartomány

domain :: [(t, t1)] -> [t]
domain xs = map (\(a,_) -> a) xs

-- értékkészlet

range :: [(t, t1)] -> [t1]
range xs = map (\(_,b) -> b) xs

-- inverz

invert :: [(t, t1)] -> [(t1, t)]
invert xs = map (\(a,b) -> (b,a)) xs

-- kép

image :: (Eq t) => [(t, t1)] -> [t] -> [t1]
image xs ys = range ( xs ! ys ) -- todo chk

-- elem képe

imgMem :: (Eq t) => [(t, t1)] -> t -> [t1]
imgMem xs y = range ( filter (\(x,_) -> x == y) xs ) -- todo chk

-- inverz kép

invImg :: (Eq t1) => [(t, t1)] -> [t1] -> [t]
invImg xs ys = image (invert xs) ys -- todo chk

-- elem inverz képe

invMem :: (Eq t1) => [(t, t1)] -> t1 -> [t]
invMem xs y = imgMem (invert xs) y -- todo chk

-- xs leszűkítése h-ra

(!) :: (Eq t) => [(t, t1)] -> [t] -> [(t, t1)]
xs ! h = filter (\(x,_) -> x ∈ h) xs

-- őskép -- todo naming
-- proper inverse image ???? -- teljes inverz kép

oskep :: (Eq a, Eq a1) => [(a, a1)] -> [a1] -> [a]
oskep xs ys = filter (\a -> (imgMem xs a) ⊆ ys) (domain xs) -- todo chk
--[a | a<-(elems $ domain xs), (imgMem xs a) ⊆ ys]

-- kompozíció

(°) :: (Eq t1) => [(t1, t2)] -> [(t, t1)] -> [(t, t2)]
q ° p = [(a,d) | (a,b) <- p, (c,d) <- q, b == c]
--HUH na most jön a nemdet: q °° p = map (\(a,b) -> pffffff) (filter (\(_,b) -> b ∈ domain q) p) 

-- szigorú kompozíció

(°!) :: (Eq t) => [(t, t1)] -> [(t, t)] -> [(t, t1)]
q °! p = [(a,d) | (a,b) <- p, (c,d) <- q, a == b, imgMem p a ⊆ domain q]

-- identikus

id :: [a] -> [(a, a)]
id xs = map (\x -> (x,x)) xs

-- lezártja : todo

{-lezar xs a b = -- rel ⊆ a×b
  where
    dLezart = filter -}

-- korlátos lezártja


-- igazsághalmaz

ighalm :: (Eq a) => [(a, Bool)] -> [a]
ighalm xs = oskep xs [True]

ighalm' :: [(t, Bool)] -> [t]
ighalm' xs = invMem xs True

-- megszorított

megsz :: (Eq a) => [(a, a)] -> [(a, Bool)] -> [(a, a)]
xs `megsz` pi = xs ! igPi ∪ igPiMinDxs
  where
    igPi = ighalm pi
    igPiMinDxs = id (igPi \\ (domain xs))